nat{-}deq $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$<\lambda$$a$,$b$. ($a$ =$_{0}$ $b$), TERMOF\{nat{-}deq{-}aux:ObjectId, 1:l\}$>$